; EXPECT: sat
(set-option :incremental false)
(set-logic ALL)

(declare-fun x () (Relation Int Int))
(declare-fun y () (Relation Int Int))
(declare-fun z () (Relation Int Int))
(declare-fun w () (Relation Int Int))
(assert (= z (rel.tclosure x)))
(assert (= w (rel.join x y)))
(assert (set.member (tuple 2 2) z))
(assert (set.member (tuple 0 3) y))
(assert (set.member (tuple (- 1) 3) y))
(assert (set.member (tuple 1 3) y))
(assert (set.member (tuple (- 2) 3) y))
(assert (set.member (tuple 2 3) y))
(assert (set.member (tuple 3 3) y))
(assert (set.member (tuple 4 3) y))
(assert (set.member (tuple 5 3) y))
(assert (not (set.member (tuple 2 3) (rel.join x y))))
(assert (not (set.member (tuple 2 1) x)))
(check-sat)
